Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    app(app(add,0),y)  → y
2:    app(app(add,app(s,x)),y)  → app(s,app(app(add,x),y))
3:    app(app(mult,0),y)  → 0
4:    app(app(mult,app(s,x)),y)  → app(app(add,app(app(mult,x),y)),y)
5:    app(app(app(rec,f),x),0)  → x
6:    app(app(app(rec,f),x),app(s,y))  → app(app(f,app(s,y)),app(app(app(rec,f),x),y))
7:    fact  → app(app(rec,mult),app(s,0))
There are 13 dependency pairs:
8:    APP(app(add,app(s,x)),y)  → APP(s,app(app(add,x),y))
9:    APP(app(add,app(s,x)),y)  → APP(app(add,x),y)
10:    APP(app(add,app(s,x)),y)  → APP(add,x)
11:    APP(app(mult,app(s,x)),y)  → APP(app(add,app(app(mult,x),y)),y)
12:    APP(app(mult,app(s,x)),y)  → APP(add,app(app(mult,x),y))
13:    APP(app(mult,app(s,x)),y)  → APP(app(mult,x),y)
14:    APP(app(mult,app(s,x)),y)  → APP(mult,x)
15:    APP(app(app(rec,f),x),app(s,y))  → APP(app(f,app(s,y)),app(app(app(rec,f),x),y))
16:    APP(app(app(rec,f),x),app(s,y))  → APP(f,app(s,y))
17:    APP(app(app(rec,f),x),app(s,y))  → APP(app(app(rec,f),x),y)
18:    FACT  → APP(app(rec,mult),app(s,0))
19:    FACT  → APP(rec,mult)
20:    FACT  → APP(s,0)
The approximated dependency graph contains one SCC: {9,11,13,15-17}.
Tyrolean Termination Tool  (0.11 seconds)   ---  May 3, 2006